ds:x:Id fp Type, da:k:Knd fp Type, x:ecl(ds;da). (eclthrow?(x))  (eclthrow-n(x)  ) 

latex

Definitions	x:A. B(x), P  Q, b, eclthrow?(x), t  T, , eclthrow-n(x), A  B, ff, tt, if b then t else f fi , False, A, x. t(x), ecl(ds;da), , x(s), eclbase(k;test), eclseq(a;b), ecland(a;b), eclor(a;b), [a]*, a.n, eclthrow(a;n), eclcatch(a;l)
Lemmas	false wf, true wf, le wf, assert wf, eclthrow? wf, ecl wf, fpf wf, Knd wf, Id wf